Nuprl Lemma : comb_for_fib_wf
2,24
postcript
pdf
(
n
,
z
. fib(
n
))
True
latex
Definitions
T
,
x
:
A
.
B
(
x
)
,
t
T
,
True
,
Lemmas
nat
wf
,
true
wf
,
squash
wf
,
fib
wf
origin
n,z. fib(n)) 
True n,z. fib(n)) True T
x:A. B(x) T